Starting from PAT 2.0, we applied a layered design to support the analysis of the different system/languages. The figure below shows the architecture design of PAT. For each supported system (e.g., distributed system, service oriented computing, bio-system, security protocols, sensor network and real-time system), a dedicated module is created in PAT, which identifies the (specialized) language syntax, well-formness rules as well as (operational) formal semantics. The formally defined operational semantics of the target language translates the behaviors of a model into a Labeled Transition System (LTS). During this translation, domain specific abstraction can be applied to the input model, e.g., data abstraction, zone abstraction and environment abstraction. LTS serves as the internal representations of the input models, which can be automatically explored by the verification algorithms or used for simulation. If there is any counterexample is identified, then it can be animated in the simulator. The advantage of this design allows the developed model checking algorithms to be shared by all modules.

This architecture allows new languages to be developed easily by providing the syntax rules and semantics. Till now, eleven modules have been developed, namely Communicating Sequential Processes (CSP) Module, Real-Time System Module, Probability CSP Module, Probability RTS Module, Labeled Transition System Module, Timed Automata Module, NesC Module, ORC Module, Stateflow(MDL) Module, Security Module and Web Service (WS) Module. In the future, our targeted systems include distributed systems, UML (state chart and sequence diagrams) and so on.

The main functionalities of PAT are listed as follows:

• User friendly editing environment (multi-document, multi-language, I18N GUI and advanced syntax editing features) for introducing models
• User friendly simulator for interactively and visually simulating system behaviors; by random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
• Easy verification for deadlock-freeness analysis, reachability analysis, state/event linear temporal logic checking (with or without fairness) and refinement checking.
• A wide range of built-in examples ranging from benchmark systems to newly developed algorithms/protocols.

PAT has been applied to a variety of different systems to prove properties or identifying bugs. Indeed, previously unknown bugs have been found using PAT. We have successfully demonstrated PAT as an analyzer for process algebras in the 30th International Conference on Software Engineering (ICSE 2008) [LiuSD08] and the 21st International Conference on Computer Aided Verification (CAV 2009) [SunLDP09]. In summary, PAT is a self-contained framework for automated analysis on concurrent and real-time systems.